Step of Proof: append_overlapping_sublists 11,40
Inference at * 1 2 2 1 
Iof proof for Lemma append overlapping sublists:



1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. i, j:. (i < ||L||)  (j < ||L||)  ((i = j))  ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||}{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9. j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)}{0..||L||}
11. increasing(f;||L2||+1)
12. j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||[]||  0 
  increasing(i.if i z ||L1|| then f1(i) else f(i - ||L1||) fi ;||L1 @ [x / L2]||) 
latex
 by InteriorProof ((((((((((((Unfold `increasing` 0) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN (
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
CollapseTHEN () inil_term)))) 
CollapseTHEN (SplitOnConclITE))) 
CollapseTHENA (
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok SupInf:t
CollapseTHENA () inil_term)))) 
CollapseTHEN (SplitOnConclITE))) 
CollapseTHEN (
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t
CollapseTHEN () inil_term))) 
latex

C1: .....truecase..... NILNIL

C1: 15. i : {0..(||L1 @ [x / L2]|| - 1)}
C1: 16. i  ||L1||
C1: 17. (i+1)  ||L1||
C1:   (f1(i)) < (f1(i+1))
C2: .....falsecase..... NILNIL

C2: 15. i : {0..(||L1 @ [x / L2]|| - 1)}
C2: 16. i  ||L1||
C2: 17. ||L1|| < (i+1)
C2:   (f1(i)) < (f((i+1) - ||L1||))
C3: .....falsecase..... NILNIL

C3: 15. i : {0..(||L1 @ [x / L2]|| - 1)}
C3: 16. ||L1|| < i
C3: 17. ||L1|| < (i+1)
C3:   (f(i - ||L1||)) < (f((i+1) - ||L1||))
C.

Definitionsincreasing(f;k), T, ff, P  Q, P  Q, if b then t else f fi , tt, x:A. B(x), False, P & Q, True, , i  j < k, t  T, A  B, {i..j}, A, P  Q, Unit, , i  j ,
Lemmastrue wf, squash wf, assert of lt int, bnot of le int, eqff to assert, assert of le int, eqtt to assert, iff transitivity, append wf, int seg wf, bnot wf, lt int wf, le wf, assert wf, bool wf, length wf1, le int wf

origin